sumdeq(a;b)(p,q)
== Case p of
== inl(pa)  Case q of inl(qa)  1of(a)(pa,qa) ; inr(qb)  false
== inr(pb)  Case q of inl(qa)  false ; inr(qb)  1of(b)(pb,qb) 

latex

Definitions	1of(t), false
FDL editor aliases	sumdeq